3.9.2.1 Alarm Monitor

3.9.2.1 Alarm Monitor

An alarm controller system is designed to fulfill two functions: one is to lock car doors when speed exceeds 20, and the other is to turn on an alarm when speed is larger than 10 while the seat belt is not worn. The following Stateflow diagram modeling this alarm monitor system consists of two parallel states, state SpeedOmeter updating variable speed based on events timeTic and roadTic, and state Car specifying the dynamic behavior of the monitor. A driver can toggle engine between on and off. When the engine turns on (in state EngineOn), initially the monitor is at state Stopped. Once speed is greater than 0, the monitor becomes active by entering state Running that contains two parallel substates: state Belts can raise an alarm based on the belt status and speed when it is activated, and state Locks deals with the lock of doors. Note that all events guarding transitions are inputs from environment (for instance, event toggle is decided by a driver).

Our PAT model that is automatically generated is available here. The model preserves the hierarchical structure and captures the complex execution order of the diagram. We add six assertions to this PAT model; these assertions specify the desired properties of the alarm monitor system such as whether car speed can exceed 20. Besides assertions, we also tune the PAT model for the efficiency during verification. To be specific, we constrain the speed value from 0 to 21, and the value of belt to be 0 or 1. An auxiliary variable EngineOn_Entry indicates the complete of the entry action of state EngineOn. The fine-tuned PAT model is avialable here. Using the PAT model checker, we can exhaustively examine all possible situations that the alarm monitor system may encounter. Furthermore the verification process is fully automated. With the help of PAT, we found that this alarm monitor system failed to satisfy the desired properties that are denoted by the following assertions.

//engineOn => (speed > 20 => locksDown)
     #define goal2 !(Car_EngineOn_Status == active && EngineOn_Entry == 1)
                    || !(speed > 20)
                    || (Car_EngineOn_Running_Locks_LocksOn_Status == active);
     #assert Stateflow() |= [] goal2;

    //engineOn => ((speed > 10 && belt <> 0) => alarm = 1)
    #define goal3 !(Car_EngineOn_Status == active && EngineOn_Entry == 1)
                   || !(speed > 1 && belt == notoccurred)
                   || (Car_EngineON_Running_Belts_Status == active);
    #assert Stateflow() |= [] goal3;

For example, the first property (goal2) requires the door must be locked when the engine is on and the speed exceeds 20. The counterexample that is automatically generated by PAT demonstrates the following scenario: a car's speed reaches beyond 20 when its engine is off (for example, the car moves on a slope), when the driver toggles the engine from off to on, the default sub-state Stopped is entered, and therefore the event locksDown is not able to be generated. To fix the problem, we adopt the solution proposed by Scaife et al., which is to add conditions when entering default states. Reusing the previous example, the default transition to state Stopped is guarded by condition [speed = 0] and another condition [speed > 0] is added to guard a new default transition to state Running. Similarly, the default transition to state LocksOff is constrained by condition [speed <= 20] while condition [speed > 20] is inserted to guard a new default transition to state LocksOn.